\begin{tabbing}
f{-}newround\=\{\$x:ut2, \$free:ut2, \$mine:ut2\}\+
\\[0ex](${\it es}$; $L$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=((loc($e$) $\in$ $L$) $\wedge$ @$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$free:ut2\}))\+
\\[0ex]$\wedge$ (es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$mine:ut2\})
\-
\end{tabbing}